#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_enumeration.h"
namespace CVC4 {
-bool CegqiOutputSingleInv::doAddInstantiation( std::vector< Node >& subs ) {
- return d_out->doAddInstantiation( subs );
-}
-
-bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) {
- return d_out->isEligibleForInstantiation( n );
-}
-
-bool CegqiOutputSingleInv::addLemma( Node n ) {
- return d_out->addLemma( n );
-}
-
CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p)
: d_qe(qe),
d_parent(p),
d_sip(new SingleInvocationPartition),
d_sol(new CegSingleInvSol(qe)),
- d_cosi(new CegqiOutputSingleInv(this)),
- d_cinst(new CegInstantiator(d_qe, d_cosi, false, false)),
- d_c_inst_match_trie(NULL),
d_single_invocation(false)
{
- // The third and fourth arguments of d_cosi set to (false,false) until we have
- // solution reconstruction for delta and infinity.
- if (options::incrementalSolving()) {
- d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext());
- }
}
CegSingleInv::~CegSingleInv()
{
- if (d_c_inst_match_trie) {
- delete d_c_inst_match_trie;
- }
- delete d_cosi;
delete d_sol; // (new CegSingleInvSol(qe)),
delete d_sip; // d_sip(new SingleInvocationPartition),
}
-void CegSingleInv::getInitialSingleInvLemma(Node g, std::vector<Node>& lems)
-{
- Assert(!g.isNull());
- Assert(!d_single_inv.isNull());
- // make for new var/sk
- d_single_inv_var.clear();
- d_single_inv_sk.clear();
- Node inst;
- NodeManager* nm = NodeManager::currentNM();
- if (d_single_inv.getKind() == FORALL)
- {
- for (unsigned i = 0, size = d_single_inv[0].getNumChildren(); i < size; i++)
- {
- std::stringstream ss;
- ss << "k_" << d_single_inv[0][i];
- Node k = nm->mkSkolem(ss.str(),
- d_single_inv[0][i].getType(),
- "single invocation function skolem");
- d_single_inv_var.push_back(d_single_inv[0][i]);
- d_single_inv_sk.push_back(k);
- d_single_inv_sk_index[k] = i;
- }
- inst = d_single_inv[1].substitute(d_single_inv_var.begin(),
- d_single_inv_var.end(),
- d_single_inv_sk.begin(),
- d_single_inv_sk.end());
- }
- else
- {
- inst = d_single_inv;
- }
- inst = TermUtil::simpleNegate(inst);
- Trace("cegqi-si") << "Single invocation initial lemma : " << inst
- << std::endl;
-
- // register with the instantiator
- Node ginst = nm->mkNode(OR, g.negate(), inst);
- lems.push_back(ginst);
- // make and register the instantiator
- d_cinst.reset(new CegInstantiator(d_qe, d_cosi, false, false));
- d_cinst->registerCounterexampleLemma(lems, d_single_inv_sk);
-}
-
void CegSingleInv::initialize(Node q)
{
// can only register one quantified formula with this
}
// we now have determined whether we will do single invocation techniques
- if( d_single_invocation ){
- d_single_inv = d_sip->getSingleInvocation();
- d_single_inv = TermUtil::simpleNegate( d_single_inv );
- std::vector<Node> func_vars;
- d_sip->getFunctionVariables(func_vars);
- if (!func_vars.empty())
- {
- Node pbvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, func_vars);
- d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv );
- }
- //now, introduce the skolems
- std::vector<Node> sivars;
- d_sip->getSingleInvocationVariables(sivars);
- for (unsigned i = 0, size = sivars.size(); i < size; i++)
- {
- Node v = NodeManager::currentNM()->mkSkolem(
- "a", sivars[i].getType(), "single invocation arg");
- d_single_inv_arg_sk.push_back( v );
- }
- d_single_inv = d_single_inv.substitute(sivars.begin(),
- sivars.end(),
- d_single_inv_arg_sk.begin(),
- d_single_inv_arg_sk.end());
- Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv << std::endl;
- // check whether we can handle this quantified formula
- CegHandledStatus status = CegInstantiator::isCbqiQuant(d_single_inv);
- if( status<CEG_HANDLED )
- {
- Trace("cegqi-si") << "...do not invoke single invocation techniques since the quantified formula does not have a handled counterexample-guided instantiation strategy!" << std::endl;
- d_single_invocation = false;
- d_single_inv = Node::null();
- }
- else if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){
- //just invoke the presolve now
- d_cinst->presolve( d_single_inv );
- }
- }
- if( !d_single_invocation )
+ if (!d_single_invocation)
{
d_single_inv = Node::null();
Trace("cegqi-si") << "Formula is not single invocation." << std::endl;
ss << "Property is not handled by single invocation." << std::endl;
throw LogicException(ss.str());
}
+ return;
}
-}
-
-bool CegSingleInv::doAddInstantiation(std::vector<Node>& subs)
-{
- Assert( d_single_inv_sk.size()==subs.size() );
- Trace("cegqi-si-inst-debug") << "CegSingleInv::doAddInstantiation, #vars = ";
- Trace("cegqi-si-inst-debug") << d_single_inv_sk.size() << "..." << std::endl;
- std::stringstream siss;
- if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){
- siss << " * single invocation: " << std::endl;
- for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){
- Node op = d_sip->getFunctionForFirstOrderVariable(d_single_inv[0][j]);
- Assert(!op.isNull());
- siss << " * " << op;
- siss << " (" << d_single_inv_sk[j] << ")";
- siss << " -> " << subs[j] << std::endl;
- }
+ NodeManager* nm = NodeManager::currentNM();
+ d_single_inv = d_sip->getSingleInvocation();
+ d_single_inv = TermUtil::simpleNegate(d_single_inv);
+ std::vector<Node> func_vars;
+ d_sip->getFunctionVariables(func_vars);
+ if (!func_vars.empty())
+ {
+ Node pbvl = nm->mkNode(BOUND_VAR_LIST, func_vars);
+ // mark as quantifier elimination to ensure its structure is preserved
+ Node n_attr =
+ nm->mkSkolem("qe_si",
+ nm->booleanType(),
+ "Auxiliary variable for qe attr for single invocation.");
+ QuantElimAttribute qea;
+ n_attr.setAttribute(qea, true);
+ n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
+ n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr);
+ // make the single invocation conjecture
+ d_single_inv = nm->mkNode(FORALL, pbvl, d_single_inv, n_attr);
}
- Trace("cegqi-si-inst-debug") << siss.str();
-
- bool alreadyExists;
- Node lem;
- if( subs.empty() ){
- Assert( d_single_inv.getKind()!=FORALL );
- alreadyExists = false;
- lem = d_single_inv;
- }else{
- Assert( d_single_inv.getKind()==FORALL );
- if( options::incrementalSolving() ){
- alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() );
- }else{
- alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs );
- }
- Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl;
- //Trace("cegqi-si-inst-debug") << siss.str();
- //Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl;
- if( alreadyExists ){
- return false;
- }else{
- Trace("cegqi-engine") << siss.str() << std::endl;
- Assert( d_single_inv_var.size()==subs.size() );
- lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
- if( d_qe->getTermUtil()->containsVtsTerm( lem ) ){
- Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl;
- lem = d_qe->getTermUtil()->rewriteVtsSymbols( lem );
- }
- }
+ // now, introduce the skolems
+ std::vector<Node> sivars;
+ d_sip->getSingleInvocationVariables(sivars);
+ for (unsigned i = 0, size = sivars.size(); i < size; i++)
+ {
+ Node v = NodeManager::currentNM()->mkSkolem(
+ "a", sivars[i].getType(), "single invocation arg");
+ d_single_inv_arg_sk.push_back(v);
}
- Trace("cegqi-engine-debug") << "Rewrite..." << std::endl;
- lem = Rewriter::rewrite( lem );
- Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
- if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){
- d_curr_lemmas.push_back( lem );
- d_lemmas_produced.push_back( lem );
- d_inst.push_back( std::vector< Node >() );
- d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() );
+ d_single_inv = d_single_inv.substitute(sivars.begin(),
+ sivars.end(),
+ d_single_inv_arg_sk.begin(),
+ d_single_inv_arg_sk.end());
+ Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv
+ << std::endl;
+ // check whether we can handle this quantified formula
+ CegHandledStatus status = CegInstantiator::isCbqiQuant(d_single_inv);
+ if (status < CEG_HANDLED)
+ {
+ Trace("cegqi-si") << "...do not invoke single invocation techniques since "
+ "the quantified formula does not have a handled "
+ "counterexample-guided instantiation strategy!"
+ << std::endl;
+ d_single_invocation = false;
+ d_single_inv = Node::null();
}
- return true;
}
-
-bool CegSingleInv::isEligibleForInstantiation(Node n)
+bool CegSingleInv::solve()
{
- return n.getKind()!=SKOLEM || std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end();
-}
-
-bool CegSingleInv::addLemma(Node n)
-{
- d_curr_lemmas.push_back( n );
- return true;
-}
-
-bool CegSingleInv::check(std::vector<Node>& lems)
-{
- if( !d_single_inv.isNull() ) {
- Trace("cegqi-si-debug") << "CegSingleInv::check..." << std::endl;
- Trace("cegqi-si-debug")
- << "CegSingleInv::check consulting ceg instantiation..." << std::endl;
- d_curr_lemmas.clear();
- Assert( d_cinst!=NULL );
- //call check for instantiator
- d_cinst->check();
- Trace("cegqi-si-debug") << "...returned " << d_curr_lemmas.size() << " lemmas " << std::endl;
- //add lemmas
- lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
- return !lems.empty();
- }else{
- // not single invocation
+ if (d_single_inv.isNull())
+ {
+ // not using single invocation techniques
return false;
}
-}
-
-Node CegSingleInv::constructSolution(std::vector<unsigned>& indices,
- unsigned i,
- unsigned index,
- std::map<Node, Node>& weak_imp)
-{
- Assert( index<d_inst.size() );
- Assert( i<d_inst[index].size() );
- unsigned uindex = indices[index];
- if( index==indices.size()-1 ){
- return d_inst[uindex][i];
- }else{
- Node cond = d_lemmas_produced[uindex];
- //weaken based on unsat core
- std::map< Node, Node >::iterator itw = weak_imp.find( cond );
- if( itw!=weak_imp.end() ){
- cond = itw->second;
+ Trace("cegqi-si") << "Solve using single invocation..." << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
+ // solve the single invocation conjecture using a fresh copy of SMT engine
+ SmtEngine siSmt(nm->toExprManager());
+ siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
+ siSmt.assertFormula(d_single_inv.toExpr());
+ Result r = siSmt.checkSat();
+ Trace("cegqi-si") << "Result: " << r << std::endl;
+ if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+ {
+ // conjecture is infeasible or unknown
+ return false;
+ }
+ // now, get the instantiations
+ std::vector<Expr> qs;
+ siSmt.getInstantiatedQuantifiedFormulas(qs);
+ Assert(qs.size() <= 1);
+ // track the instantiations, as solution construction is based on this
+ Trace("cegqi-si") << "#instantiated quantified formulas=" << qs.size()
+ << std::endl;
+ d_inst.clear();
+ d_instConds.clear();
+ for (const Expr& q : qs)
+ {
+ TNode qn = Node::fromExpr(q);
+ Assert(qn.getKind() == FORALL);
+ std::vector<std::vector<Expr> > tvecs;
+ siSmt.getInstantiationTermVectors(q, tvecs);
+ Trace("cegqi-si") << "#instantiations of " << q << "=" << tvecs.size()
+ << std::endl;
+ std::vector<Node> vars;
+ for (const Node& v : qn[0])
+ {
+ vars.push_back(v);
+ }
+ Node body = qn[1];
+ for (unsigned i = 0, ninsts = tvecs.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));
+ }
+ Trace("cegqi-si") << " Instantiation: " << inst << std::endl;
+ d_inst.push_back(inst);
+ Assert(inst.size() == vars.size());
+ Node ilem =
+ body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end());
+ ilem = Rewriter::rewrite(ilem);
+ d_instConds.push_back(ilem);
+ Trace("cegqi-si") << " Instantiation Lemma: " << ilem << std::endl;
}
- cond = TermUtil::simpleNegate( cond );
- Node ite1 = d_inst[uindex][i];
- Node ite2 = constructSolution( indices, i, index+1, weak_imp );
- return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
}
+ return true;
}
//TODO: use term size?
bool rconsSygus)
{
Assert( d_sol!=NULL );
- Assert( !d_lemmas_produced.empty() );
+ Assert(!d_inst.empty());
const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
Node varList = Node::fromExpr( dt.getSygusVarList() );
Node prog = d_quant[0][sol_index];
//construct the solution
Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl;
- bool useUnsatCore = false;
- std::vector< Node > active_lemmas;
- //minimize based on unsat core, if possible
- std::map< Node, Node > weak_imp;
- if( options::cegqiSolMinCore() ){
- if( options::cegqiSolMinInst() ){
- if( d_qe->getUnsatCoreLemmas( active_lemmas, weak_imp ) ){
- useUnsatCore = true;
- }
- }else{
- if( d_qe->getUnsatCoreLemmas( active_lemmas ) ){
- useUnsatCore = true;
- }
- }
- }
- Assert( d_lemmas_produced.size()==d_inst.size() );
std::vector< unsigned > indices;
- for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){
- bool incl = true;
- if( useUnsatCore ){
- incl = std::find( active_lemmas.begin(), active_lemmas.end(), d_lemmas_produced[i] )!=active_lemmas.end();
- }
- if( incl ){
- Assert( sol_index<d_inst[i].size() );
- indices.push_back( i );
- }
+ for (unsigned i = 0, ninst = d_inst.size(); i < ninst; i++)
+ {
+ indices.push_back(i);
}
- Trace("csi-sol") << "...included " << indices.size() << " / " << d_lemmas_produced.size() << " instantiations." << std::endl;
Assert( !indices.empty() );
//sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions)
// TODO : to minimize solution size, put the largest term last
ssii.d_i = sol_index;
std::sort( indices.begin(), indices.end(), ssii );
Trace("csi-sol") << "Construct solution" << std::endl;
- s = constructSolution( indices, sol_index, 0, weak_imp );
+ std::reverse(indices.begin(), indices.end());
+ s = d_inst[indices[0]][sol_index];
+ // it is an ITE chain whose conditions are the instantiations
+ NodeManager* nm = NodeManager::currentNM();
+ for (unsigned j = 1, nindices = indices.size(); j < nindices; j++)
+ {
+ unsigned uindex = indices[j];
+ Node cond = d_instConds[uindex];
+ cond = TermUtil::simpleNegate(cond);
+ s = nm->mkNode(ITE, cond, d_inst[uindex][sol_index], s);
+ }
Assert( vars.size()==d_sol->d_varList.size() );
s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() );
}
namespace quantifiers {
class SynthConjecture;
-class CegSingleInv;
-
-class CegqiOutputSingleInv : public CegqiOutput {
- public:
- CegqiOutputSingleInv(CegSingleInv* out) : d_out(out) {}
- virtual ~CegqiOutputSingleInv() {}
- CegSingleInv* d_out;
- bool doAddInstantiation(std::vector<Node>& subs) override;
- bool isEligibleForInstantiation(Node n) override;
- bool addLemma(Node lem) override;
-};
class DetTrace {
private:
std::vector< Node >& terms,
std::map< Node, std::vector< Node > >& teq,
Node n, std::vector< Node >& conj );
- // constructing solution
- Node constructSolution(std::vector<unsigned>& indices, unsigned i,
- unsigned index, std::map<Node, Node>& weak_imp);
Node postProcessSolution(Node n);
private:
/** pointer to the quantifiers engine */
std::map< Node, TransitionInference > d_ti;
// solution reconstruction
CegSingleInvSol* d_sol;
- // the instantiator's output channel
- CegqiOutputSingleInv* d_cosi;
- // the instantiator
- std::unique_ptr<CegInstantiator> d_cinst;
// list of skolems for each argument of programs
std::vector<Node> d_single_inv_arg_sk;
std::map<Node, int> d_single_inv_sk_index;
// program to solution index
std::map<Node, unsigned> d_prog_to_sol_index;
- // lemmas produced
- inst::InstMatchTrie d_inst_match_trie;
- inst::CDInstMatchTrie* d_c_inst_match_trie;
// original conjecture
Node d_orig_conjecture;
// solution
Node d_solution;
Node d_sygus_solution;
public:
- // lemmas produced
- std::vector<Node> d_lemmas_produced;
+ /**
+ * The list of instantiations that suffice to show the first-order equivalent
+ * of the negated synthesis conjecture is unsatisfiable.
+ */
std::vector<std::vector<Node> > d_inst;
+ /**
+ * The list of instantiation lemmas, corresponding to instantiations of the
+ * first order conjecture for the term vectors above.
+ */
+ std::vector<Node> d_instConds;
private:
- std::vector<Node> d_curr_lemmas;
- // add instantiation
- bool doAddInstantiation( std::vector< Node >& subs );
- //is eligible for instantiation
- bool isEligibleForInstantiation( Node n );
- // add lemma
- bool addLemma( Node lem );
// conjecture
Node d_quant;
Node d_simp_quant;
// get simplified conjecture
Node getSimplifiedConjecture() { return d_simp_quant; }
public:
- /** get the single invocation lemma(s)
- *
- * This adds lemmas to lem that initializes this class for doing
- * counterexample-guided instantiation for the synthesis conjecture. These
- * lemmas correspond to the negation of the body of the (anti-skolemized)
- * form of the conjecture for fresh skolems.
- *
- * Argument g is guard, for which all the above lemmas are guarded.
- */
- void getInitialSingleInvLemma(Node g, std::vector<Node>& lems);
// initialize this class for synthesis conjecture q
void initialize( Node q );
/** finish initialize
*
* This method sets up final decisions about whether to use single invocation
- * techniques. The argument syntaxRestricted is whether the syntax for
- * solutions for the initialized conjecture is restricted.
+ * techniques.
+ *
+ * The argument syntaxRestricted is whether the syntax for solutions for the
+ * initialized conjecture is restricted.
*/
void finishInit(bool syntaxRestricted);
- //check
- bool check( std::vector< Node >& lems );
+ /** solve
+ *
+ * If single invocation techniques are being used, it solves
+ * the first order form of the negated synthesis conjecture using a fresh
+ * copy of the SMT engine. This method returns true if it has successfully
+ * found a solution to the synthesis conjecture using this method.
+ */
+ bool solve();
//get solution
Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus = true );
//reconstruct to syntax
projects / cvc5.git / commitdiff