diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-12 11:14:08 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-12 11:14:08 -0500 |
commit | 3ce6e00068c02286704143d82d5f044fdb356516 (patch) | |
tree | 53d8403a8cc2c92db4cb815861f5c7cd56dee446 /src/theory/quantifiers | |
parent | e93c443a0bfb1a66909e8467b24da399be3d01ac (diff) |
Eliminate uses of Expr in SmtEngine interface (#5240)
This eliminates all use of Expr in the SmtEngine except in a few interfaces (setUserAttribute, getAssignment) whose signature is currently in question.
The next steps will be to (1) eliminate Expr from the smt/model.h interface, (2) replace Type by TypeNode in Sort.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 24 |
1 files changed, 8 insertions, 16 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 4ab92f6a7..4b45072f7 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -386,7 +386,7 @@ bool CegSingleInv::solve() return false; } // now, get the instantiations - std::vector<Expr> qs; + std::vector<Node> qs; siSmt->getInstantiatedQuantifiedFormulas(qs); Assert(qs.size() <= 1); // track the instantiations, as solution construction is based on this @@ -394,15 +394,13 @@ bool CegSingleInv::solve() << std::endl; d_inst.clear(); d_instConds.clear(); - for (const Expr& q : qs) + for (const Node& q : qs) { - TNode qn = Node::fromExpr(q); - Assert(qn.getKind() == FORALL); - std::vector<std::vector<Expr> > tvecs; - siSmt->getInstantiationTermVectors(q, tvecs); - Trace("sygus-si") << "#instantiations of " << q << "=" << tvecs.size() + Assert(q.getKind() == FORALL); + siSmt->getInstantiationTermVectors(q, d_inst); + Trace("sygus-si") << "#instantiations of " << q << "=" << d_inst.size() << std::endl; - // We use the original synthesis conjecture siq, since qn may contain + // We use the original synthesis conjecture siq, since q may contain // internal symbols e.g. termITE skolem after preprocessing. std::vector<Node> vars; for (const Node& v : siq[0]) @@ -410,16 +408,10 @@ bool CegSingleInv::solve() vars.push_back(v); } Node body = siq[1]; - for (unsigned i = 0, ninsts = tvecs.size(); i < ninsts; i++) + for (unsigned i = 0, ninsts = d_inst.size(); i < ninsts; i++) { - std::vector<Expr>& tvi = tvecs[i]; - std::vector<Node> inst; - for (const Expr& t : tvi) - { - inst.push_back(Node::fromExpr(t)); - } + std::vector<Node>& inst = d_inst[i]; Trace("sygus-si") << " Instantiation: " << inst << std::endl; - d_inst.push_back(inst); // instantiation should have same arity since we are not allowed to // eliminate variables from quantifiers marked with QuantElimAttribute. Assert(inst.size() == vars.size()); |