namespace theory {
namespace datatypes {
-TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo)
+TheoryDatatypes::TheoryDatatypes(Context* c,
+ UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo)
: Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
- //d_cycle_check(c),
- d_hasSeenCycle(c, false),
d_infer(c),
d_infer_exp(c),
- d_term_sk( u ),
- d_notify( *this ),
+ d_term_sk(u),
+ d_notify(*this),
d_equalityEngine(d_notify, c, "theory::datatypes", true),
- d_labels( c ),
- d_selector_apps( c ),
- //d_consEqc( c ),
- d_conflict( c, false ),
- d_collectTermsCache( c ),
- d_functionTerms( c ),
- d_singleton_eq( u ),
- d_lemmas_produced_c( u )
+ d_labels(c),
+ d_selector_apps(c),
+ d_conflict(c, false),
+ d_addedLemma(false),
+ d_addedFact(false),
+ d_collectTermsCache(c),
+ d_functionTerms(c),
+ d_singleton_eq(u),
+ d_lemmas_produced_c(u)
{
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
void TheoryDatatypes::eqNotifyNewClass(TNode t){
if( t.getKind()==APPLY_CONSTRUCTOR ){
getOrMakeEqcInfo( t, true );
- //look at all equivalence classes with constructor terms
-/*
- for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){
- if( (*it).second ){
- TNode r = (*it).first;
- if( r.getType()==t.getType() ){
- EqcInfo * ei = getOrMakeEqcInfo( r, false );
- if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){
- Node deq = ei->d_constructor.get().eqNode( t ).negate();
- d_pending.push_back( deq );
- d_pending_exp[ deq ] = d_true;
- Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl;
- d_infer.push_back( deq );
- }
- }
- }
- }
-*/
- //d_consEqc[t] = true;
}
}
if( d_conflict ){
return;
}
- //d_consEqc[t1] = true;
}
- //AJR: do this?
- //else if( cons2.isConst() ){
- // //prefer the constant
- // eqc1->d_constructor = cons2;
- //}
- //d_consEqc[t2] = false;
}
}else{
Trace("datatypes-debug") << " no eqc info for " << t1 << ", must create" << std::endl;
for( unsigned i=0; i<ncons.getNumChildren(); i++ ) {
TNode cn = searchForCycle( ncons[i], on, visited, proc, explanation, false );
if( cn==on ) {
- //if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){
- // Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl;
- //}
//add explanation for why the constructor is connected
if( n != ncons ) {
explainEquality( n, ncons, true, explanation );
typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
- /** transitive closure to record equivalence/subterm relation. */
- // TransitiveClosureNode d_cycle_check;
- /** has seen cycle */
- context::CDO<bool> d_hasSeenCycle;
/** inferences */
NodeList d_infer;
NodeList d_infer_exp;
/** selector apps for eqch equivalence class */
NodeIntMap d_selector_apps;
std::map< Node, std::vector< Node > > d_selector_apps_data;
- /** constructor terms */
- //BoolMap d_consEqc;
/** Are we in conflict */
context::CDO<bool> d_conflict;
- /** Added lemma ? */
+ /** added lemma
+ *
+ * This flag is set to true during a full effort check if this theory
+ * called d_out->lemma(...).
+ */
bool d_addedLemma;
+ /** added fact
+ *
+ * This flag is set to true during a full effort check if this theory
+ * added an internal fact to its equality engine.
+ */
bool d_addedFact;
/** The conflict node */
Node d_conflictNode;
};
BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn)
- : Instantiator(qe, tn)
+ : Instantiator(qe, tn), d_inst_id_counter(0)
{
// get the global inverter utility
// this must be global since we need to:
#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
-InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
- : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ),
-d_elim_quants( qe->getSatContext() ),
-d_nested_qe_waitlist_size( qe->getUserContext() ),
-d_nested_qe_waitlist_proc( qe->getUserContext() )
+InstStrategyCbqi::InstStrategyCbqi(QuantifiersEngine* qe)
+ : QuantifiersModule(qe),
+ d_cbqi_set_quant_inactive(false),
+ d_incomplete_check(false),
+ d_added_cbqi_lemma(qe->getUserContext()),
+ d_elim_quants(qe->getSatContext()),
+ d_nested_qe_waitlist_size(qe->getUserContext()),
+ d_nested_qe_waitlist_proc(qe->getUserContext())
//, d_added_inst( qe->getUserContext() )
{
d_qid_count = 0;
typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
protected:
+ /** set quantified formula inactive
+ *
+ * This flag is set to true during a full effort check if at least one
+ * quantified formula is set "inactive", that is, its negation is
+ * unsatisfiable in the current context.
+ */
bool d_cbqi_set_quant_inactive;
+ /** incomplete check
+ *
+ * This is set to true during a full effort check if this strategy could
+ * not find an instantiation for at least one asserted quantified formula.
+ */
bool d_incomplete_check;
/** whether we have added cbqi lemma */
NodeSet d_added_cbqi_lemma;
}
}
-
-
-ConjectureGenerator::ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ),
-d_notify( *this ),
-d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
-d_ee_conjectures( c ){
- d_fullEffortCount = 0;
- d_conj_count = 0;
- d_subs_confirmCount = 0;
- d_subs_unkCount = 0;
+ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
+ context::Context* c)
+ : QuantifiersModule(qe),
+ d_notify(*this),
+ d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
+ d_ee_conjectures(c),
+ d_conj_count(0),
+ d_subs_confirmCount(0),
+ d_subs_unkCount(0),
+ d_fullEffortCount(0),
+ d_hasAddedLemma(false)
+{
d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR );
class TermGenerator
{
-private:
+ private:
unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs );
-public:
- TermGenerator(){}
+
+ public:
+ TermGenerator()
+ : d_id(0),
+ d_status(0),
+ d_status_num(0),
+ d_match_status(0),
+ d_match_status_child_num(0),
+ d_match_mode(0)
+ {
+ }
TypeNode d_typ;
unsigned d_id;
//1 : consider as unique variable
return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
}
-CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) :
-CandidateGenerator( qe ), d_term_iter( -1 ){
+CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
+ : CandidateGenerator(qe), d_term_iter(-1), d_term_iter_limit(0)
+{
d_op = qe->getTermDatabase()->getMatchOperator( pat );
Assert( !d_op.isNull() );
}
d_eval_uf_use_default.clear();
d_eval_uf_model.clear();
d_eval_term_index_order.clear();
- d_eval_formulas = 0;
- d_eval_uf_terms = 0;
- d_eval_lits = 0;
- d_eval_lits_unknown = 0;
}
//if evaluate( n ) = eVal,
// if eVal is not 0, then
// each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
- ++d_eval_formulas;
Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl;
//Notice() << "Eval " << n << std::endl;
if( n.getKind()==NOT ){
}else if( n.getKind()==FORALL ){
return 0;
}else{
- ++d_eval_lits;
//Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
int retVal = 0;
depIndex = ri->getNumTerms()-1;
if( retVal!=0 ){
Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl;
}else{
- ++d_eval_lits_unknown;
Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
Trace("fmf-eval-amb") << " value : " << val << std::endl;
}
//Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
//if it is a defined UF, then consult the interpretation
if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
- ++d_eval_uf_terms;
int argDepIndex = 0;
//make the term model specifically for n
makeEvalUfModel( n );
/** evaluate functions */
int evaluate( Node n, int& depIndex, RepSetIterator* ri );
Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri );
-public:
- //statistics
- int d_eval_formulas;
- int d_eval_uf_terms;
- int d_eval_lits;
- int d_eval_lits_unknown;
private:
//default evaluate term function
Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri );
return false;
}
-QModelBuilderIG::Statistics::Statistics():
- d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
- d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
- d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ),
- d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ),
- d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ),
- d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ),
- d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
- d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
+QModelBuilderIG::Statistics::Statistics()
+ : d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
+ d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers",
+ 0),
+ d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0),
+ d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0)
{
smtStatisticsRegistry()->registerStat(&d_num_quants_init);
smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init);
smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas);
smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas);
- smtStatisticsRegistry()->registerStat(&d_eval_formulas);
- smtStatisticsRegistry()->registerStat(&d_eval_uf_terms);
- smtStatisticsRegistry()->registerStat(&d_eval_lits);
- smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown);
}
QModelBuilderIG::Statistics::~Statistics(){
smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init);
smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas);
smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas);
- smtStatisticsRegistry()->unregisterStat(&d_eval_formulas);
- smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms);
- smtStatisticsRegistry()->unregisterStat(&d_eval_lits);
- smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown);
}
//do exhaustive instantiation
}
}
//print debugging information
- if( fmig ){
- d_statistics.d_eval_formulas += fmig->d_eval_formulas;
- d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
- d_statistics.d_eval_lits += fmig->d_eval_lits;
- d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
- }
Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl;
Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl;
Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl;
IntStat d_num_partial_quants_init;
IntStat d_init_inst_gen_lemmas;
IntStat d_inst_gen_lemmas;
- IntStat d_eval_formulas;
- IntStat d_eval_uf_terms;
- IntStat d_eval_lits;
- IntStat d_eval_lits_unknown;
Statistics();
~Statistics();
};
TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
context::Context* c,
- context::UserContext* u):
- d_rels(NULL),
- d_members(c),
- d_deq(c),
- d_deq_processed(u),
- d_keep(c),
- d_proxy(u),
- d_proxy_to_term(u),
- d_lemmas_produced(u),
- d_card_processed(u),
- d_var_elim(u),
- d_external(external),
- d_notify(*this),
- d_equalityEngine(d_notify, c, "theory::sets::ee", true),
- d_conflict(c)
+ context::UserContext* u)
+ : d_members(c),
+ d_deq(c),
+ d_deq_processed(u),
+ d_keep(c),
+ d_sentLemma(false),
+ d_addedFact(false),
+ d_full_check_incomplete(false),
+ d_proxy(u),
+ d_proxy_to_term(u),
+ d_lemmas_produced(u),
+ d_card_enabled(false),
+ d_card_processed(u),
+ d_var_elim(u),
+ d_external(external),
+ d_notify(*this),
+ d_equalityEngine(d_notify, c, "theory::sets::ee", true),
+ d_conflict(c),
+ d_rels(
+ new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external)),
+ d_rels_enabled(false)
{
-
- d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external);
-
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
d_equalityEngine.addFunctionKind(kind::MEMBER);
d_equalityEngine.addFunctionKind(kind::SUBSET);
- // If cardinality is on.
d_equalityEngine.addFunctionKind(kind::CARD);
-
- d_card_enabled = false;
- d_rels_enabled = false;
-
-}/* TheorySetsPrivate::TheorySetsPrivate() */
+}
TheorySetsPrivate::~TheorySetsPrivate(){
- delete d_rels;
for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) {
delete current_pair.second;
}
-}/* TheorySetsPrivate::~TheorySetsPrivate() */
-
+}
void TheorySetsPrivate::eqNotifyNewClass(TNode t) {
if( t.getKind()==kind::SINGLETON || t.getKind()==kind::EMPTYSET ){
typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
-private:
- TheorySetsRels * d_rels;
public:
void eqNotifyNewClass(TNode t);
void eqNotifyPreMerge(TNode t1, TNode t2);
void addEqualityToExp( Node a, Node b, std::vector< Node >& exp );
void debugPrintSet( Node s, const char * c );
-
+
+ /** sent lemma
+ *
+ * This flag is set to true during a full effort check if this theory
+ * called d_out->lemma(...).
+ */
bool d_sentLemma;
+ /** added fact
+ *
+ * This flag is set to true during a full effort check if this theory
+ * added an internal fact to its equality engine.
+ */
bool d_addedFact;
+ /** full check incomplete
+ *
+ * This flag is set to true during a full effort check if this theory
+ * is incomplete for some reason (for instance, if we combine cardinality
+ * with a relation or extended function kind).
+ */
bool d_full_check_incomplete;
NodeMap d_proxy;
NodeMap d_proxy_to_term;
std::map< Kind, std::map< Node, std::map< Node, Node > > > d_bop_index;
std::map< Kind, std::vector< Node > > d_op_list;
//cardinality
-private:
+ private:
+ /** is cardinality enabled?
+ *
+ * This flag is set to true during a full effort check if any constraint
+ * involving cardinality constraints is asserted to this theory.
+ */
bool d_card_enabled;
/** element types of sets for which cardinality is enabled */
std::map<TypeNode, bool> d_t_card_enabled;
- bool d_rels_enabled;
std::map< Node, Node > d_eqc_to_card_term;
NodeSet d_card_processed;
std::map< Node, std::vector< Node > > d_card_parent;
bool isCareArg( Node n, unsigned a );
public:
bool isEntailed( Node n, bool pol );
-
+
+ private:
+ /** subtheory solver for the theory of relations */
+ std::unique_ptr<TheorySetsRels> d_rels;
+ /** are relations enabled?
+ *
+ * This flag is set to true during a full effort check if any constraint
+ * involving relational constraints is asserted to this theory.
+ */
+ bool d_rels_enabled;
};/* class TheorySetsPrivate */
projects / cvc5.git / commitdiff