Elizabeth Polgreen and Andrew Reynolds and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2021-10

April 13, 2021

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-10.pdf

In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification) phase. Many synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) solvers to provide counterexamples. But what if a white-box oracle is either not available or not easy to work with?

We present a framework for solving a general class of oracle-guided synthesis problems which we term synthesis modulo oracles. In this setting, oracles may be black boxes with a query-response interface defined by the synthesis problem. As a necessary component of this framework, we also formalize the problem of satisfiability modulo oracles, and present an algorithm for solving this problem.

We show that our algorithm for solving synthesis modulo oracles is expressive enough to execute several algorithms for synthesis and verification including CEGIS and ICE learning. We implement the first prototype solver for satisfiability and synthesis modulo oracles and, with an image transformation case study, demonstrate applicability to problems using complex oracles that incorporate compilation and execution of code.

---

BibTeX citation:

@techreport{Polgreen:EECS-2021-10,
    Author= {Polgreen, Elizabeth and Reynolds, Andrew and Seshia, Sanjit A.},
    Title= {Satisfiability and Synthesis Modulo Oracles},
    Year= {2021},
    Month= {Apr},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-10.html},
    Number= {UCB/EECS-2021-10},
    Abstract= {In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification) phase. Many synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) solvers to provide counterexamples. But what if a white-box oracle is either not available or not easy to work with? 

We present a framework for solving a general class of oracle-guided synthesis problems which we term synthesis modulo oracles. In this setting, oracles may be black boxes with a query-response interface defined by the synthesis problem. As a necessary component of this framework, we also formalize the problem of satisfiability modulo oracles, and present an algorithm for solving this problem.

We show that our algorithm for solving synthesis modulo oracles is expressive enough to execute several algorithms for synthesis and verification including CEGIS and ICE learning. We implement the first prototype solver for satisfiability and synthesis modulo oracles and, with an image transformation case study,  demonstrate applicability to problems using complex oracles that incorporate compilation and execution of code.},
}

EndNote citation:

%0 Report
%A Polgreen, Elizabeth 
%A Reynolds, Andrew 
%A Seshia, Sanjit A. 
%T Satisfiability and Synthesis Modulo Oracles
%I EECS Department, University of California, Berkeley
%D 2021
%8 April 13
%@ UCB/EECS-2021-10
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-10.html
%F Polgreen:EECS-2021-10