From 22b211647501a4dad5cec66c2ea6383ea8e7b7bd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 9 Nov 2017 09:51:52 -0600 Subject: [PATCH] Decouple sygus term database and term database. (#1317) * Decouple sygus term database and term database. * Clang format * Fix include --- src/theory/quantifiers/term_database.cpp | 14 +------ .../quantifiers/term_database_sygus.cpp | 42 +++++++++++-------- src/theory/quantifiers/term_database_sygus.h | 4 ++ src/theory/quantifiers_engine.cpp | 19 +++++++-- 4 files changed, 44 insertions(+), 35 deletions(-) diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a3225e404..5db58067f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -14,20 +14,12 @@ #include "theory/quantifiers/term_database.h" -#include "expr/datatype.h" #include "options/base_options.h" #include "options/quantifiers_options.h" -#include "options/datatypes_options.h" #include "options/uf_options.h" -#include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fun_def_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/rewrite_engine.h" -#include "theory/quantifiers/theory_quantifiers.h" -#include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" @@ -250,10 +242,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi d_ops.push_back(op); d_op_map[op].push_back( n ); added.insert( n ); - - if( d_quantEngine->getTermDatabaseSygus() ){ - d_quantEngine->getTermDatabaseSygus()->registerEvalTerm( n ); - } } }else{ setTermInactive( n ); diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index f298e9711..d8d120eab 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -1912,32 +1912,38 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) { void TermDbSygus::registerEvalTerm( Node n ) { if( options::sygusDirectEval() ){ if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){ - Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n - << std::endl; TypeNode tn = n[0].getType(); if( tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); if( dt.isSygus() ){ Node f = n.getOperator(); - Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl; if( n[0].getKind()!=APPLY_CONSTRUCTOR ){ - d_evals[n[0]].push_back( n ); - TypeNode tn = n[0].getType(); - Assert( tn.isDatatype() ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Node var_list = Node::fromExpr( dt.getSygusVarList() ); - Assert( dt.isSygus() ); - d_eval_args[n[0]].push_back( std::vector< Node >() ); - bool isConst = true; - for( unsigned j=1; j()); + bool isConst = true; + for (unsigned j = 1; j < n.getNumChildren(); j++) + { + d_eval_args[n[0]].back().push_back(n[j]); + if (!n[j].isConst()) + { + isConst = false; + } } + d_eval_args_const[n[0]].push_back(isConst); + Node a = getAnchor(n[0]); + d_subterms[a][n[0]] = true; } - d_eval_args_const[n[0]].push_back( isConst ); - Node a = getAnchor( n[0] ); - d_subterms[a][n[0]] = true; } } } diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h index c819bc781..4786f053b 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/term_database_sygus.h @@ -17,6 +17,8 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H +#include + #include "theory/quantifiers/sygus_explain.h" #include "theory/quantifiers/term_database.h" @@ -243,6 +245,8 @@ public: // for symmetry breaking //for eager instantiation // TODO (as part of #1235) move some of these functions to sygus_explain.h private: + /** the set of evaluation terms we have already processed */ + std::unordered_set d_eval_processed; std::map< Node, std::map< Node, bool > > d_subterms; std::map< Node, std::vector< Node > > d_evals; std::map< Node, std::vector< std::vector< Node > > > d_eval_args; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ac0de29e3..f6b920cda 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -854,10 +854,21 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within std::set< Node > added; d_term_db->addTerm(n, added, withinQuant, withinInstClosure); - //added contains also the Node that just have been asserted in this branch - if( d_quant_rel ){ - for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ - if( !withinQuant ){ + if (!withinQuant) + { + if (d_sygus_tdb) + { + d_sygus_tdb->registerEvalTerm(n); + } + + // added contains also the Node that just have been asserted in this + // branch + if (d_quant_rel) + { + for (std::set::iterator i = added.begin(), end = added.end(); + i != end; + i++) + { d_quant_rel->setRelevance( i->getOperator(), 0 ); } } -- 2.30.2