diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-18 11:41:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-18 11:41:46 -0500 |
commit | ab9742939d7706e10ea3d70c73275e97a5235f03 (patch) | |
tree | d7d08da62cc172bdd8940357c27d848dc9e3c04c /src/theory/quantifiers | |
parent | c460fd4ba1cdacf04305475e605071889ed0e92f (diff) |
Split SygusSolver from SmtEngine (#4891)
This is the solver for standard SyGuS queries. Notice it now depends only on SmtSolver and not SmtEngine.
This PR updates Expr -> Node for the sygus interface in SmtEngine.
SmtEnginePrivate is no longer needed and is deleted with this PR.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_interpol.cpp | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 0d08140d3..0ecd888e0 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -274,10 +274,10 @@ void SygusInterpol::mkSygusConjecture(Node itp, bool SygusInterpol::findInterpol(Expr& interpol, Node itp) { // get the synthesis solution - std::map<Expr, Expr> sols; + std::map<Node, Node> sols; d_subSolver->getSynthSolutions(sols); Assert(sols.size() == 1); - std::map<Expr, Expr>::iterator its = sols.find(itp.toExpr()); + std::map<Node, Node>::iterator its = sols.find(itp); if (its == sols.end()) { Trace("sygus-interpol") @@ -288,7 +288,7 @@ bool SygusInterpol::findInterpol(Expr& interpol, Node itp) } Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is " << its->second << std::endl; - Node interpoln = Node::fromExpr(its->second); + Node interpoln = its->second; // replace back the created variables to original symbols. Node interpoln_reduced; if (interpoln.getKind() == kind::LAMBDA) @@ -336,18 +336,17 @@ bool SygusInterpol::SolveInterpolation(const std::string& name, createVariables(itpGType.isNull()); for (Node var : d_vars) { - d_subSolver->declareSygusVar(name, var.toExpr(), var.getType().toType()); + d_subSolver->declareSygusVar(name, var, var.getType()); } - std::vector<Expr> vars_empty; + std::vector<Node> vars_empty; TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj); Node itp = mkPredicate(name); - d_subSolver->declareSynthFun( - name, itp.toExpr(), grammarType.toType(), false, vars_empty); + d_subSolver->declareSynthFun(name, itp, grammarType, false, vars_empty); mkSygusConjecture(itp, axioms, conj); Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : " << d_sygusConj << ", solving for " - << d_sygusConj[0][0].toExpr() << std::endl; - d_subSolver->assertSygusConstraint(d_sygusConj.toExpr()); + << d_sygusConj[0][0] << std::endl; + d_subSolver->assertSygusConstraint(d_sygusConj); Trace("sygus-interpol") << " SmtEngine::getInterpol check sat..." << std::endl; |