diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 14:06:52 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 14:07:11 -0500 |
commit | f3590092818d9eab9d961ea602093029ff472a85 (patch) | |
tree | 1401f00df0d9659ba2321ea2088fe0c3f4de9f52 /src/smt/smt_engine.cpp | |
parent | d598a9644862d176632071bca8448765d9cc3cc1 (diff) |
Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e9e21fb48..6960c4684 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -89,6 +89,7 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/term_database.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" #include "theory/substitutions.h" @@ -4605,11 +4606,17 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx if( conj.getKind()==kind::FORALL ){ //possibly run quantifier elimination to make formula into single invocation if( conj[1].getKind()==kind::EXISTS ){ - Node conj_se = conj[1][1]; + Node conj_se = Node::fromExpr( expandDefinitions( conj[1][1].toExpr() ) ); Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl; - quantifiers::SingleInvocationPartition sip( kind::APPLY ); - sip.init( conj_se ); + quantifiers::SingleInvocationPartition sip; + std::vector< Node > funcs; + for( unsigned i=0; i<conj[0].getNumChildren(); i++ ){ + Node sf = conj[0][i].getAttribute(theory::SygusSynthFunAttribute()); + Assert( !sf.isNull() ); + funcs.push_back( sf ); + } + sip.init( funcs, conj_se ); Trace("smt-synth") << "...finished, got:" << std::endl; sip.debugPrint("smt-synth"); |