diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-14 13:23:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-14 13:23:07 -0500 |
commit | c130a81b3578898dcb5cacaf746e4dd923e2c5d6 (patch) | |
tree | 167e9bf516882cfb6c08f88b9110ca241a973f6a /src/smt | |
parent | 94af13b18b10d6092981848fbae1b9c35b27b31d (diff) |
Call separate SMT engine for single invocation sygus (#3151)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 16 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 26 |
2 files changed, 30 insertions, 12 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 27ee446fe..78f47993f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1321,14 +1321,6 @@ void SmtEngine::setDefaults() { options::unconstrainedSimp.set(uncSimp); } } - if (!options::proof()) - { - // minimizing solutions from single invocation requires proofs - if (options::cegqiSolMinCore() && options::cegqiSolMinCore.wasSetByUser()) - { - throw OptionException("cegqi-si-sol-min-core requires --proof"); - } - } // Disable options incompatible with unsat cores and proofs or output an // error if enabled explicitly @@ -1804,8 +1796,12 @@ void SmtEngine::setDefaults() { Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl; options::cbqi.set(false); } - //track instantiations? - if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas.wasSetByUser() ) ){ + // Do we need to track instantiations? + // Needed for sygus due to single invocation techniques. + if (options::cbqiNestedQE() + || (options::proof() && !options::trackInstLemmas.wasSetByUser()) + || is_sygus) + { options::trackInstLemmas.set( true ); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index eba73c380..4ac21d392 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -587,11 +587,33 @@ class CVC4_PUBLIC SmtEngine /** Same as above, but without user-provided grammar restrictions */ bool getAbduct(const Expr& conj, Expr& abd); - /** Get list of quantified formulas that were instantiated. */ + /** + * Get list of quantified formulas that were instantiated on the last call + * to check-sat. + */ void getInstantiatedQuantifiedFormulas(std::vector<Expr>& qs); - /** Get instantiations. */ + /** + * Get instantiations for quantified formula q. + * + * If q was a quantified formula that was instantiated on the last call to + * check-sat (i.e. q is returned as part of the vector in the method + * getInstantiatedQuantifiedFormulas above), then the list of instantiations + * of that formula that were generated are added to insts. + * + * In particular, if q is of the form forall x. P(x), then insts is a list + * of formulas of the form P(t1), ..., P(tn). + */ void getInstantiations(Expr q, std::vector<Expr>& insts); + /** + * Get instantiation term vectors for quantified formula q. + * + * This method is similar to above, but in the example above, we return the + * (vectors of) terms t1, ..., tn instead. + * + * Notice that these are not guaranteed to come in the same order as the + * instantiation lemmas above. + */ void getInstantiationTermVectors(Expr q, std::vector<std::vector<Expr> >& tvecs); |