diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_inference.cpp | 21 |
2 files changed, 23 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 116d2fe23..15b6e2fc9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1403,6 +1403,8 @@ void SmtEngine::setDefaults() { d_logic = d_logic.getUnlockedCopy(); d_logic.enableTheory(THEORY_DATATYPES); d_logic.lock(); + // since we are trying to recast as sygus, we assume the input is sygus + is_sygus = true; } if ((options::checkModels() || options::checkSynthSol()) @@ -2053,6 +2055,10 @@ void SmtEngine::setDefaults() { if( !options::miniscopeQuantFreeVar.wasSetByUser() ){ options::miniscopeQuantFreeVar.set( false ); } + if (!options::quantSplit.wasSetByUser()) + { + options::quantSplit.set(false); + } //rewrite divk if( !options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); diff --git a/src/theory/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp index fe5761e03..6232de6fe 100644 --- a/src/theory/quantifiers/sygus_inference.cpp +++ b/src/theory/quantifiers/sygus_inference.cpp @@ -144,6 +144,13 @@ bool SygusInference::simplify(std::vector<Node>& assertions) free_functions.push_back(op); } } + else if (cur.getKind() == VARIABLE) + { + // a free variable is a 0-argument function to synthesize + Assert(std::find(free_functions.begin(), free_functions.end(), cur) + == free_functions.end()); + free_functions.push_back(cur); + } else if (cur.getKind() == FORALL) { Trace("sygus-infer") @@ -159,7 +166,7 @@ bool SygusInference::simplify(std::vector<Node>& assertions) processed_assertions.push_back(pas); } - // if no free function symbols, there is no use changing into SyGuS + // no functions to synthesize if (free_functions.empty()) { Trace("sygus-infer") << "...fail: no free function symbols." << std::endl; @@ -252,16 +259,22 @@ bool SygusInference::simplify(std::vector<Node>& assertions) if (itffv != ff_var_to_ff.end()) { Node ff = itffv->second; + Expr body = it->second; std::vector<Expr> args; - for (const Node& v : lambda[0]) + // if it is a non-constant function + if (lambda.getKind() == LAMBDA) { - args.push_back(v.toExpr()); + for (const Node& v : lambda[0]) + { + args.push_back(v.toExpr()); + } + body = it->second[1]; } Trace("sygus-infer") << "Define " << ff << " as " << it->second << std::endl; final_ff.push_back(ff); final_ff_sol.push_back(it->second); - master_smte->defineFunction(ff.toExpr(), args, it->second[1]); + master_smte->defineFunction(ff.toExpr(), args, body); } } |