diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-10 23:27:39 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-10 23:27:45 +0200 |
commit | 089d232454e89dc44a6ca2136f9b408c9335d8f1 (patch) | |
tree | 21c815088431e820ccc3b3e42fa05e5a5a9bea68 /src/theory | |
parent | 859ab54a3cc8afdc01980e3e97e91b45480586dc (diff) |
Initial draft of CEGQI.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 181 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 43 | ||||
-rwxr-xr-x | src/theory/quantifiers/conjecture_generator.cpp | 54 | ||||
-rwxr-xr-x | src/theory/quantifiers/conjecture_generator.h | 13 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 21 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 35 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 30 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 11 |
11 files changed, 315 insertions, 104 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index fec4255b2..f4cdd1a60 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -27,21 +27,190 @@ using namespace std; namespace CVC4 { -CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) { +CegInstantiation::CegConjecture::CegConjecture() { +} + +void CegInstantiation::CegConjecture::assign( Node q ) { + Assert( d_quant.isNull() ); + Assert( q.getKind()==FORALL ); + d_quant = q; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) ); + } +} +void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ + if( d_guard.isNull() ){ + d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); + //specify guard behavior + qe->getValuation().ensureLiteral( d_guard ); + qe->getOutputChannel().requirePhase( d_guard, true ); + } +} + +CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), d_conj_active( c, false ), d_conj_infeasible( c, false ), d_guard_assertions( c ) { - +} + +bool CegInstantiation::needsCheck( Theory::Effort e ) { + return e>=Theory::EFFORT_LAST_CALL; } void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { - //TODO + if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ + Trace("cegqi-engine") << "---Countexample Guided Instantiation Engine---" << std::endl; + Trace("cegqi-debug") << "Current conjecture status : " << d_conj_active << " " << d_conj_infeasible << std::endl; + if( d_conj_active && !d_conj_infeasible ){ + checkCegConjecture( &d_conj ); + } + Trace("cegqi-engine") << "Finished Countexample Guided Instantiation engine." << std::endl; + } } void CegInstantiation::registerQuantifier( Node q ) { - //TODO + if( d_quantEngine->getOwner( q )==this ){ + if( !d_conj.isAssigned() ){ + Trace("cegqi") << "Register conjecture : " << q << std::endl; + d_conj.assign( q ); + //construct base instantiation + d_conj.d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj.d_candidates ) ); + Trace("cegqi") << "Base instantiation is : " << d_conj.d_base_inst << std::endl; + if( getTermDatabase()->isQAttrSygus( q ) ){ + Assert( d_conj.d_base_inst.getKind()==NOT ); + Assert( d_conj.d_base_inst[0].getKind()==FORALL ); + for( unsigned j=0; j<d_conj.d_base_inst[0][0].getNumChildren(); j++ ){ + d_conj.d_inner_vars.push_back( d_conj.d_base_inst[0][0][j] ); + } + }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ + //add immediate lemma + Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_base_inst ); + } + }else{ + Assert( d_conj.d_quant==q ); + } + } } void CegInstantiation::assertNode( Node n ) { - + Trace("cegqi-debug") << "Cegqi : Assert : " << n << std::endl; + bool pol = n.getKind()!=NOT; + Node lit = n.getKind()==NOT ? n[0] : n; + if( lit==d_conj.d_guard ){ + d_guard_assertions[lit] = pol; + d_conj_infeasible = !pol; + } + if( lit==d_conj.d_quant ){ + d_conj_active = true; + } +} + +Node CegInstantiation::getNextDecisionRequest() { + d_conj.initializeGuard( d_quantEngine ); + bool value; + if( !d_quantEngine->getValuation().hasSatValue( d_conj.d_guard, value ) ) { + if( d_guard_assertions.find( d_conj.d_guard )==d_guard_assertions.end() ){ + if( d_conj.d_guard_split.isNull() ){ + Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_guard ); + d_quantEngine->getOutputChannel().lemma( lem ); + } + Trace("cegqi-debug") << "Decide next on : " << d_conj.d_guard << "..." << std::endl; + return d_conj.d_guard; + } + } + return Node::null(); +} + +void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { + Node q = conj->d_quant; + Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl; + Trace("cegqi-engine-debug") << " * Candidate program/output : "; + for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ + Trace("cegqi-engine-debug") << conj->d_candidates[i] << " "; + } + Trace("cegqi-engine-debug") << std::endl; + + if( getTermDatabase()->isQAttrSygus( q ) ){ + Trace("cegqi-engine-debug") << " * Values are : "; + bool success = true; + std::vector< Node > model_values; + for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ + Node v = getModelValue( conj->d_candidates[i] ); + model_values.push_back( v ); + Trace("cegqi-engine-debug") << v << " "; + if( v.isNull() ){ + success = false; + } + } + Trace("cegqi-engine-debug") << std::endl; + + if( success ){ + //must get a counterexample to the value of the current candidate + Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); + inst = Rewriter::rewrite( inst ); + //body should be an existential + Assert( inst.getKind()==NOT ); + Assert( inst[0].getKind()==FORALL ); + //immediately skolemize + Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] ); + Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl; + d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) ); + + //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate + Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[inst[0]].size() ); + Node inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(), + getTermDatabase()->d_skolem_constants[inst[0]].begin(), getTermDatabase()->d_skolem_constants[inst[0]].end() ); + Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine.negate() ); + Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl; + d_quantEngine->addLemma( lem ); + } + + }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ + std::vector< Node > model_terms; + for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ + Node t = getModelTerm( conj->d_candidates[i] ); + model_terms.push_back( t ); + } + d_quantEngine->addInstantiation( q, model_terms, false ); + } } - + +Node CegInstantiation::getModelValue( Node n ) { + Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; + //return d_quantEngine->getTheoryEngine()->getModelValue( n ); + TypeNode tn = n.getType(); + if( getEqualityEngine()->hasTerm( n ) ){ + Node r = getRepresentative( n ); + Node v; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() ); + while( !eqc_i.isFinished() ){ + TNode nn = (*eqc_i); + if( nn.isConst() ){ + Trace("cegqi-mv") << "..constant : " << nn << std::endl; + return nn; + }else if( nn.getKind()==APPLY_CONSTRUCTOR ){ + v = nn; + } + ++eqc_i; + } + if( !v.isNull() ){ + std::vector< Node > children; + if( v.hasOperator() ){ + children.push_back( v.getOperator() ); + } + for( unsigned i=0; i<v.getNumChildren(); i++ ){ + children.push_back( getModelValue( v[i] ) ); + } + Node vv = NodeManager::currentNM()->mkNode( v.getKind(), children ); + Trace("cegqi-mv") << "...value : " << vv << std::endl; + return vv; + } + } + Node e = getTermDatabase()->getEnumerateTerm( tn, 0 ); + Trace("cegqi-mv") << "...enumerate : " << e << std::endl; + return e; +} + +Node CegInstantiation::getModelTerm( Node n ){ + return getModelValue( n ); +} + }
\ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 7861deffa..6139f8f59 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -25,16 +25,59 @@ namespace CVC4 { namespace theory { namespace quantifiers { + + class CegInstantiation : public QuantifiersModule { + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; +private: + class CegConjecture { + public: + CegConjecture(); + /** quantified formula */ + Node d_quant; + /** guard */ + Node d_guard; + /** base instantiation */ + Node d_base_inst; + /** guard split */ + Node d_guard_split; + /** list of constants for quantified formula */ + std::vector< Node > d_candidates; + /** list of variables on inner quantification */ + std::vector< Node > d_inner_vars; + /** is assigned */ + bool isAssigned() { return !d_quant.isNull(); } + /** assign */ + void assign( Node q ); + /** initialize guard */ + void initializeGuard( QuantifiersEngine * qe ); + }; + /** the quantified formula stating the synthesis conjecture */ + CegConjecture d_conj; + /** is conjecture active */ + context::CDO< bool > d_conj_active; + /** is conjecture infeasible */ + context::CDO< bool > d_conj_infeasible; + /** assertions for guards */ + NodeBoolMap d_guard_assertions; +private: + /** check conjecture */ + void checkCegConjecture( CegConjecture * conj ); + /** get model value */ + Node getModelValue( Node n ); + /** get model term */ + Node getModelTerm( Node n ); public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); public: + bool needsCheck( Theory::Effort e ); /* Call during quantifier engine's check */ void check( Theory::Effort e, unsigned quant_e ); /* Called for new quantifiers */ void registerQuantifier( Node q ); void assertNode( Node n ); + Node getNextDecisionRequest(); /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "CegInstantiation"; } }; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index fe3c92323..f491adc7c 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -280,33 +280,6 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) { }
}
-eq::EqualityEngine * ConjectureGenerator::getEqualityEngine() {
- return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
-}
-
-bool ConjectureGenerator::areEqual( TNode n1, TNode n2 ) {
- eq::EqualityEngine * ee = getEqualityEngine();
- return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) );
-}
-
-bool ConjectureGenerator::areDisequal( TNode n1, TNode n2 ) {
- eq::EqualityEngine * ee = getEqualityEngine();
- return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false );
-}
-
-TNode ConjectureGenerator::getRepresentative( TNode n ) {
- eq::EqualityEngine * ee = getEqualityEngine();
- if( ee->hasTerm( n ) ){
- return ee->getRepresentative( n );
- }else{
- return n;
- }
-}
-
-TermDb * ConjectureGenerator::getTermDatabase() {
- return d_quantEngine->getTermDatabase();
-}
-
Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
Assert( !tn.isNull() );
while( d_free_var[tn].size()<=i ){
@@ -1098,27 +1071,6 @@ int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNo }
}
-Node ConjectureGenerator::getEnumerateTerm( TypeNode tn, unsigned index ) {
- std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );
- unsigned teIndex;
- if( it==d_typ_enum_map.end() ){
- teIndex = (int)d_typ_enum.size();
- d_typ_enum_map[tn] = teIndex;
- d_typ_enum.push_back( TypeEnumerator(tn) );
- }else{
- teIndex = it->second;
- }
- while( index>=d_enum_terms[tn].size() ){
- if( d_typ_enum[teIndex].isFinished() ){
- return Node::null();
- }
- d_enum_terms[tn].push_back( *d_typ_enum[teIndex] );
- ++d_typ_enum[teIndex];
- }
- return d_enum_terms[tn][index];
-}
-
-
Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn );
if( it==d_typ_pred.end() ){
@@ -1149,7 +1101,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< vec.push_back( size_limit );
}else{
//see if we can iterate current
- if( vec_sum<size_limit && !getEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){
+ if( vec_sum<size_limit && !getTermDatabase()->getEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){
vec[index]++;
vec_sum++;
vec.push_back( size_limit - vec_sum );
@@ -1164,7 +1116,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< }
if( success ){
if( vec.size()==n.getNumChildren() ){
- Node lc = getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] );
+ Node lc = getTermDatabase()->getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] );
if( !lc.isNull() ){
for( unsigned i=0; i<vec.size(); i++ ){
Trace("sg-gt-enum-debug") << vec[i] << " ";
@@ -1177,7 +1129,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< std::vector< Node > children;
children.push_back( n.getOperator() );
for( unsigned i=0; i<(vec.size()-1); i++ ){
- Node nn = getEnumerateTerm( n[i].getType(), vec[i] );
+ Node nn = getTermDatabase()->getEnumerateTerm( n[i].getType(), vec[i] );
Assert( !nn.isNull() );
Assert( nn.getType()==n[i].getType() );
children.push_back( nn );
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 23e2b88ba..59d908fec 100755 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -357,13 +357,6 @@ public: //for generalization // get generalization depth
int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv );
private:
- //ground term enumeration
- std::map< TypeNode, std::vector< Node > > d_enum_terms;
- //type enumerators
- std::map< TypeNode, unsigned > d_typ_enum_map;
- std::vector< TypeEnumerator > d_typ_enum;
- //get nth term for type
- Node getEnumerateTerm( TypeNode tn, unsigned index );
//predicate for type
std::map< TypeNode, Node > d_typ_pred;
//get predicate for type
@@ -389,12 +382,6 @@ public: //for property enumeration std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain;
//number of ground substitutions whose equality is unknown
unsigned d_subs_unkCount;
-public: //for ground equivalence classes
- eq::EqualityEngine * getEqualityEngine();
- bool areDisequal( TNode n1, TNode n2 );
- bool areEqual( TNode n1, TNode n2 );
- TNode getRepresentative( TNode n );
- TermDb * getTermDatabase();
private: //information about ground equivalence classes
TNode d_bool_eqc[2];
std::map< TNode, Node > d_ground_eqc_map;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 060994379..8136bf11e 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1851,27 +1851,6 @@ void QuantConflictFind::assertNode( Node q ) { }
}
-eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {
- //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
- return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
-}
-bool QuantConflictFind::areEqual( Node n1, Node n2 ) {
- return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );
-}
-bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {
- return n1!=n2 && getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );
-}
-Node QuantConflictFind::getRepresentative( Node n ) {
- if( getEqualityEngine()->hasTerm( n ) ){
- return getEqualityEngine()->getRepresentative( n );
- }else{
- return n;
- }
-}
-TermDb* QuantConflictFind::getTermDatabase() {
- return d_quantEngine->getTermDatabase();
-}
-
Node QuantConflictFind::evaluateTerm( Node n ) {
if( MatchGen::isHandledUfTerm( n ) ){
Node f = MatchGen::getOperator( this, n );
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index d8f1c8e6f..81f31fa90 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -187,11 +187,6 @@ private: NodeList d_qassert;
std::map< Node, QuantInfo > d_qinfo;
private: //for equivalence classes
- eq::EqualityEngine * getEqualityEngine();
- bool areDisequal( Node n1, Node n2 );
- bool areEqual( Node n1, Node n2 );
- Node getRepresentative( Node n );
- TermDb* getTermDatabase();
// type -> list(eqc)
std::map< TypeNode, std::vector< TNode > > d_eqcs;
std::map< TypeNode, Node > d_model_basis;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 405b3749d..9c1eeb9b4 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -751,6 +751,27 @@ Node TermDb::getSkolemizedBody( Node f ){ return d_skolem_body[ f ]; } +Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { + std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn ); + unsigned teIndex; + if( it==d_typ_enum_map.end() ){ + teIndex = (int)d_typ_enum.size(); + d_typ_enum_map[tn] = teIndex; + d_typ_enum.push_back( TypeEnumerator(tn) ); + }else{ + teIndex = it->second; + } + while( index>=d_enum_terms[tn].size() ){ + if( d_typ_enum[teIndex].isFinished() ){ + return Node::null(); + } + d_enum_terms[tn].push_back( *d_typ_enum[teIndex] ); + ++d_typ_enum[teIndex]; + } + return d_enum_terms[tn][index]; +} + + Node TermDb::getFreeVariableForInstConstant( Node n ){ TypeNode tn = n.getType(); if( d_free_vars.find( tn )==d_free_vars.end() ){ @@ -983,6 +1004,7 @@ Node TermDb::getRewriteRule( Node q ) { void TermDb::computeAttributes( Node q ) { if( q.getNumChildren()==3 ){ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ + Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl; if( q[2][i].getKind()==INST_ATTRIBUTE ){ Node avar = q[2][i][0]; if( avar.getAttribute(AxiomAttribute()) ){ @@ -994,13 +1016,22 @@ void TermDb::computeAttributes( Node q ) { d_qattr_conjecture[q] = true; } if( avar.getAttribute(SygusAttribute()) ){ + //should be nested existential + Assert( q[1].getKind()==NOT ); + Assert( q[1][0].getKind()==FORALL ); Trace("quant-attr") << "Attribute : sygus : " << q << std::endl; d_qattr_sygus[q] = true; + if( d_quantEngine->getCegInstantiation()==NULL ){ + Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; + } d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); } if( avar.getAttribute(SynthesisAttribute()) ){ Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl; d_qattr_synthesis[q] = true; + if( d_quantEngine->getCegInstantiation()==NULL ){ + Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; + } d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); } if( avar.hasAttribute(QuantInstLevelAttribute()) ){ @@ -1012,7 +1043,11 @@ void TermDb::computeAttributes( Node q ) { Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl; } if( avar.getKind()==REWRITE_RULE ){ + Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; Assert( i==0 ); + if( d_quantEngine->getRewriteEngine()==NULL ){ + Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl; + } //set rewrite engine as owner d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() ); } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 3bd0563b6..25ef9c81c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -19,6 +19,7 @@ #include "expr/attribute.h" #include "theory/theory.h" +#include "theory/type_enumerator.h" #include <map> @@ -241,6 +242,8 @@ public: public: //get bound variables in n static void getBoundVars( Node n, std::vector< Node >& bvs); + + //for skolem private: /** map from universal quantifiers to their skolemized body */ @@ -253,7 +256,20 @@ public: std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ); /** get the skolemized body */ Node getSkolemizedBody( Node f); - + /** is induction variable */ + static bool isInductionTerm( Node n ); + +//for ground term enumeration +private: + /** ground terms enumerated for types */ + std::map< TypeNode, std::vector< Node > > d_enum_terms; + //type enumerators + std::map< TypeNode, unsigned > d_typ_enum_map; + std::vector< TypeEnumerator > d_typ_enum; +public: + //get nth term for type + Node getEnumerateTerm( TypeNode tn, unsigned index ); + //miscellaneous public: /** map from universal quantifiers to the list of variables */ @@ -289,11 +305,7 @@ public: int isInstanceOf( Node n1, Node n2 ); /** filter all nodes that have instances */ void filterInstances( std::vector< Node >& nodes ); - -public: //for induction - /** is induction variable */ - static bool isInductionTerm( Node n ); - + public: //general queries concerning quantified formulas wrt modules /** is quantifier treated as a rewrite rule? */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index e71489fc5..f7c4c745f 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -42,6 +42,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output d_baseDecLevel = -1; out.handleUserAttribute( "axiom", this ); out.handleUserAttribute( "conjecture", this ); + out.handleUserAttribute( "sygus", this ); + out.handleUserAttribute( "synthesis", this ); out.handleUserAttribute( "quant-inst-max-level", this ); out.handleUserAttribute( "rr-priority", this ); } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index dfa17558d..d17899cf2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -43,6 +43,34 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::inst; + +eq::EqualityEngine * QuantifiersModule::getEqualityEngine() { + return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); +} + +bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) { + eq::EqualityEngine * ee = getEqualityEngine(); + return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) ); +} + +bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) { + eq::EqualityEngine * ee = getEqualityEngine(); + return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false ); +} + +TNode QuantifiersModule::getRepresentative( TNode n ) { + eq::EqualityEngine * ee = getEqualityEngine(); + if( ee->hasTerm( n ) ){ + return ee->getRepresentative( n ); + }else{ + return n; + } +} + +quantifiers::TermDb * QuantifiersModule::getTermDatabase() { + return d_quantEngine->getTermDatabase(); +} + QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): d_te( te ), d_lemmas_produced_c(u){ @@ -184,7 +212,7 @@ void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) { QuantifiersModule * mo = getOwner( q ); if( mo!=m ){ if( mo!=NULL ){ - Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << m->identify() << ", but already has owner " << mo->identify() << "!" << std::endl; + Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << "!" << std::endl; } d_owner[q] = m; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d40277112..b5a02df60 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -37,6 +37,10 @@ namespace theory { class QuantifiersEngine; +namespace quantifiers { + class TermDb; +} + class QuantifiersModule { protected: QuantifiersEngine* d_quantEngine; @@ -61,10 +65,15 @@ public: virtual Node explain(TNode n) { return TNode::null(); } /** Identify this module (for debugging, dynamic configuration, etc..) */ virtual std::string identify() const = 0; +public: + eq::EqualityEngine * getEqualityEngine(); + bool areDisequal( TNode n1, TNode n2 ); + bool areEqual( TNode n1, TNode n2 ); + TNode getRepresentative( TNode n ); + quantifiers::TermDb * getTermDatabase(); };/* class QuantifiersModule */ namespace quantifiers { - class TermDb; class FirstOrderModel; //modules class InstantiationEngine; |