From 28b20948a3b236bf32ca399e2cd85b09c1e57e67 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 26 May 2016 14:51:01 -0500 Subject: Use term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf. --- src/theory/quantifiers/alpha_equivalence.cpp | 25 ++++++-- src/theory/quantifiers/ceg_instantiator.cpp | 35 ++++++++++- src/theory/uf/theory_uf.cpp | 92 +--------------------------- src/theory/uf/theory_uf.h | 4 +- src/theory/uf/theory_uf_strong_solver.cpp | 6 ++ src/theory/uf/theory_uf_strong_solver.h | 2 +- 6 files changed, 64 insertions(+), 100 deletions(-) (limited to 'src') diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 80066d690..a00d6d8a1 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -30,17 +30,30 @@ struct sortTypeOrder { }; Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { + std::map< Node, bool > visited; while( !tt.empty() ){ if( tt.size()==arg_index.size()+1 ){ Node t = tt.back(); - Node op = t.hasOperator() ? t.getOperator() : t; - arg_index.push_back( 0 ); + Node op; + if( t.hasOperator() ){ + if( visited.find( t )==visited.end() ){ + visited[t] = true; + op = t.getOperator(); + arg_index.push_back( 0 ); + }else{ + op = t; + arg_index.push_back( -1 ); + } + }else{ + op = t; + arg_index.push_back( 0 ); + } Trace("aeq-debug") << op << " "; aen = &(aen->d_children[op][t.getNumChildren()]); }else{ Node t = tt.back(); int i = arg_index.back(); - if( i==(int)t.getNumChildren() ){ + if( i==-1 || i==(int)t.getNumChildren() ){ tt.pop_back(); arg_index.pop_back(); }else{ @@ -56,9 +69,9 @@ Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE }else{ if( q.getNumChildren()==2 ){ //lemma ( q <=> d_quant ) - Trace("quant-ae") << "Alpha equivalent : " << std::endl; - Trace("quant-ae") << " " << q << std::endl; - Trace("quant-ae") << " " << aen->d_quant << std::endl; + Trace("alpha-eq") << "Alpha equivalent : " << std::endl; + Trace("alpha-eq") << " " << q << std::endl; + Trace("alpha-eq") << " " << aen->d_quant << std::endl; lem = q.iffNode( aen->d_quant ); }else{ //do not reduce annotated quantified formulas based on alpha equivalence diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 7489196b7..cd263e90c 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -22,6 +22,9 @@ #include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" +#include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" + //#define MBP_STRICT_ASSERTIONS using namespace std; @@ -466,6 +469,36 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: } } } + /* TODO: algebraic reasoning for bitvector instantiation + else if( pvtn.isBitVector() ){ + if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){ + for( unsigned t=0; t<2; t++ ){ + if( atom[t]==pv ){ + computeProgVars( atom[1-t] ); + if( d_inelig.find( atom[1-t] )==d_inelig.end() ){ + //only ground terms TODO: more + if( d_prog_var[atom[1-t]].empty() ){ + Node veq_c; + Node uval; + if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){ + uval = atom[1-t]; + }else{ + uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], + bv::utils::mkConst(pvtn.getConst(), 1) ); + } + if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ + subs_proc[uval][veq_c] = true; + if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + } + } + } + } + } + } + } + } + */ } } } @@ -685,7 +718,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: //[5] resort to using value in model // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype - if( ( effort>0 || pvtn.isBoolean() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){ + if( ( effort>0 || pvtn.isBoolean() || pvtn.isBitVector() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){ Node mv = getModelValue( pv ); Node pv_coeff_m; Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 5c28e4ab5..d1685bdd1 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -433,7 +433,7 @@ void TheoryUF::addSharedTerm(TNode t) { d_equalityEngine.addTriggerTerm(t, THEORY_UF); } -/* +//TODO: move quantifiers::TermArgTrie to src/theory/ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ){ if( depth==arity ){ if( t2!=NULL ){ @@ -498,13 +498,11 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg } } } -*/ void TheoryUF::computeCareGraph() { if (d_sharedTerms.size() > 0) { - -/* TODO : this does (almost) the same as below, and is 1-2 order of magnitudes faster + //use term indexing Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl; std::map< Node, quantifiers::TermArgTrie > index; std::map< Node, unsigned > arity; @@ -530,92 +528,6 @@ void TheoryUF::computeCareGraph() { Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << itii->first << "..." << std::endl; addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 ); } - */ - vector< pair > currentPairs; - - // Go through the function terms and see if there are any to split on - unsigned functionTerms = d_functionsTerms.size(); - for (unsigned i = 0; i < functionTerms; ++ i) { - - TNode f1 = d_functionsTerms[i]; - Node op = f1.getOperator(); - - for (unsigned j = i + 1; j < functionTerms; ++ j) { - - TNode f2 = d_functionsTerms[j]; - - // If the operators are not the same, we can skip this pair - if (f2.getOperator() != op) { - continue; - } - - Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; - - // If the terms are already known to be equal, we are also in good shape - if (d_equalityEngine.areEqual(f1, f2)) { - Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal, skipping" << std::endl; - continue; - } - - // We have two functions f(x1, ..., xn) and f(y1, ..., yn) no known to be equal - // We split on the argument pairs that are are not known, unless there is some - // argument pair that is already dis-equal. - bool somePairIsDisequal = false; - currentPairs.clear(); - for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { - - TNode x = f1[k]; - TNode y = f2[k]; - - Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking arguments " << x << " and " << y << std::endl; - - if (d_equalityEngine.areDisequal(x, y, false)) { - // Mark that there is a dis-equal pair and break - somePairIsDisequal = true; - Debug("uf::sharing") << "TheoryUf::computeCareGraph(): disequal, disregarding all" << std::endl; - break; - } - - if (d_equalityEngine.areEqual(x, y)) { - // We don't need this one - Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal" << std::endl; - continue; - } - - if (!d_equalityEngine.isTriggerTerm(x, THEORY_UF) || !d_equalityEngine.isTriggerTerm(y, THEORY_UF)) { - // Not connected to shared terms, we don't care - continue; - } - - // Get representative trigger terms - TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF); - TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF); - - EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared); - switch (eqStatusDomain) { - case EQUALITY_FALSE_AND_PROPAGATED: - case EQUALITY_FALSE: - case EQUALITY_FALSE_IN_MODEL: - somePairIsDisequal = true; - continue; - break; - default: - break; - // nothing - } - - // Otherwise, we need to figure it out - Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl; - currentPairs.push_back(make_pair(x_shared, y_shared)); - } - - if (!somePairIsDisequal) { - for (unsigned i = 0; i < currentPairs.size(); ++ i) { - addCarePair(currentPairs[i].first, currentPairs[i].second); - } - } - } - } } }/* TheoryUF::computeCareGraph() */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index ff7d7419a..3a83decec 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -209,8 +209,8 @@ public: StrongSolverTheoryUF* getStrongSolver() { return d_thss; } -//private: - //void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ); +private: + void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ); };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index ed28cc2fc..cda94e1c4 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1670,6 +1670,12 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, } } +StrongSolverTheoryUF::~StrongSolverTheoryUF() { + for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + delete it->second; + } +} + SortInference* StrongSolverTheoryUF::getSortInference() { return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference(); } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 11f0664f3..4e4dbef83 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -414,7 +414,7 @@ private: SubsortSymmetryBreaker* d_sym_break; public: StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th); - ~StrongSolverTheoryUF() {} + ~StrongSolverTheoryUF(); /** get theory */ TheoryUF* getTheory() { return d_th; } /** disequality propagator */ -- cgit v1.2.3 From dcb73e70575406db5ef94eb48a9ad5b2bdf7b31a Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 26 May 2016 18:19:51 -0400 Subject: Fix for aig_bitblaster.cpp --- src/theory/bv/aig_bitblaster.cpp | 25 ++++++------------------- 1 file changed, 6 insertions(+), 19 deletions(-) (limited to 'src') diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index 80a9396ac..098582433 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -19,7 +19,7 @@ #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" - +#include "smt/smt_statistics_registry.h" #ifdef CVC4_USE_ABC // Function is defined as static in ABC. Not sure how else to do this. @@ -140,23 +140,10 @@ AigBitblaster::AigBitblaster() , d_bbAtoms() , d_aigOutputNode(NULL) { - d_nullContext = new context::Context(); - switch(options::bvSatSolver()) { - case SAT_SOLVER_MINISAT: { - prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext, - "AigBitblaster"); - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - minisat->setNotify(notify); - d_satSolver = minisat; - break; - } - case SAT_SOLVER_CRYPTOMINISAT: - d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(), - "AigBitblaster"); - break; - default: - Unreachable("Unknown SAT solver type"); - } + d_nullContext = new context::Context(); + d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, smtStatisticsRegistry(), "AigBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + d_satSolver->setNotify(notify); } AigBitblaster::~AigBitblaster() { @@ -415,7 +402,7 @@ void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) { prop::SatLiteral lit(sat_variables[index-1], int_lit < 0); clause.push_back(lit); } - d_satSolver->addClause(clause, false, RULE_INVALID); + d_satSolver->addClause(clause, false); } } -- cgit v1.2.3 From d133e87221b0de3a4eb7c286cebda14548874e7c Mon Sep 17 00:00:00 2001 From: lianah Date: Thu, 26 May 2016 19:05:01 -0400 Subject: Changed aig_bitblaster to work with cryptominisat --- src/theory/bv/aig_bitblaster.cpp | 22 ++++++++++++++++++---- src/theory/bv/bitblaster_template.h | 2 +- 2 files changed, 19 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index 098582433..37e9f4476 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -140,10 +140,24 @@ AigBitblaster::AigBitblaster() , d_bbAtoms() , d_aigOutputNode(NULL) { - d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, smtStatisticsRegistry(), "AigBitblaster"); - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - d_satSolver->setNotify(notify); + d_nullContext = new context::Context(); + switch(options::bvSatSolver()) { + case SAT_SOLVER_MINISAT: { + prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext, + smtStatisticsRegistry(), + "AigBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + minisat->setNotify(notify); + d_satSolver = minisat; + break; + } + case SAT_SOLVER_CRYPTOMINISAT: + d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(), + "AigBitblaster"); + break; + default: + Unreachable("Unknown SAT solver type"); + } } AigBitblaster::~AigBitblaster() { diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index f9f5361d3..929bccada 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -306,7 +306,7 @@ class AigBitblaster : public TBitblaster { static Abc_Ntk_t* abcAigNetwork; context::Context* d_nullContext; - prop::BVSatSolverInterface* d_satSolver; + prop::SatSolver* d_satSolver; TNodeAigMap d_aigCache; NodeAigMap d_bbAtoms; -- cgit v1.2.3