From 9c4d548af9a14c18a6d69b41bba3e36054d37c0c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 16 Sep 2019 16:44:52 -0500 Subject: Move specific attributes out of term util (#3279) --- src/theory/quantifiers/fmf/bounded_integers.h | 14 ++++++++++++- src/theory/quantifiers/fmf/model_builder.cpp | 10 ++------- src/theory/quantifiers/fun_def_process.h | 15 +++++++++++--- src/theory/quantifiers/local_theory_ext.h | 10 +++++++++ src/theory/quantifiers/rewrite_engine.h | 10 +++++++++ src/theory/quantifiers/sygus/sygus_abduct.cpp | 1 + src/theory/quantifiers/sygus/sygus_grammar_cons.h | 21 +++++++++++++++++++ src/theory/quantifiers/term_util.h | 25 ----------------------- 8 files changed, 69 insertions(+), 37 deletions(-) (limited to 'src/theory') diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index d668c6f02..1333af61c 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -20,14 +20,26 @@ #include "theory/quantifiers/quant_util.h" +#include "context/cdhashmap.h" #include "context/context.h" -#include "context/context_mm.h" +#include "expr/attribute.h" namespace CVC4 { namespace theory { class RepSetIterator; +/** + * Attribute set to 1 for literals that comprise the bounds of a quantified + * formula. For example, for: + * forall x. ( 0 <= x ^ x <= n ) => P( x ) + * the literals 0 <= x and x <= n are marked 1. + */ +struct BoundIntLitAttributeId +{ +}; +typedef expr::Attribute BoundIntLitAttribute; + namespace quantifiers { class BoundedIntegers : public QuantifiersModule diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index f3eb88a90..caca25fde 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -15,19 +15,13 @@ #include "theory/quantifiers/fmf/model_builder.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" +#include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_rep_bound_ext.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/theory_uf_model.h" using namespace std; using namespace CVC4; @@ -122,7 +116,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){ } Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms); Node val = fm->getValue( n ); - if (val != d_qe->getTermUtil()->d_true) + if (!val.isConst() || !val.getConst()) { Trace("quant-check-model") << "******* Instantiation " << n << " for " << std::endl; Trace("quant-check-model") << " " << f << std::endl; diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 0282f0e40..f98208aba 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -17,15 +17,24 @@ #ifndef CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H #define CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H -#include -#include -#include #include +#include +#include "expr/attribute.h" #include "expr/node.h" #include "expr/type_node.h" namespace CVC4 { namespace theory { + +/** + * Attribute marked true for types that are used as abstraction types in + * the algorithm below. + */ +struct AbsTypeFunDefAttributeId +{ +}; +typedef expr::Attribute AbsTypeFunDefAttribute; + namespace quantifiers { //Preprocessing pass to allow finite model finding for admissible recursive function definitions diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 1cad52b43..d39ea3cfe 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -18,11 +18,21 @@ #define CVC4__THEORY__LOCAL_THEORY_EXT_H #include "context/cdo.h" +#include "expr/attribute.h" #include "expr/node_trie.h" #include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { + +/** Attribute true for quantifiers that do not need to be partially instantiated + */ +struct LtePartialInstAttributeId +{ +}; +typedef expr::Attribute + LtePartialInstAttribute; + namespace quantifiers { class LtePartialInst : public QuantifiersModule { diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 5832d2817..29aba0f1a 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -21,12 +21,22 @@ #include #include +#include "expr/attribute.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { + +/** + * An attribute for marking a priority value for rewrite rules. + */ +struct RrPriorityAttributeId +{ +}; +typedef expr::Attribute RrPriorityAttribute; + namespace quantifiers { class RewriteEngine : public QuantifiersModule diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 7e72ecb41..047a78d11 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -20,6 +20,7 @@ #include "printer/sygus_print_callback.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index b9f50f228..ca1b9ae37 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -21,6 +21,7 @@ #include #include +#include "expr/attribute.h" #include "expr/node.h" namespace CVC4 { @@ -28,6 +29,26 @@ namespace theory { class QuantifiersEngine; +/** + * Attribute for associating a function-to-synthesize with a first order + * variable whose type is a sygus datatype type that encodes its grammar. + */ +struct SygusSynthGrammarAttributeId +{ +}; +typedef expr::Attribute + SygusSynthGrammarAttribute; + +/** + * Attribute for associating a function-to-synthesize with its formal argument + * list. + */ +struct SygusSynthFunVarListAttributeId +{ +}; +typedef expr::Attribute + SygusSynthFunVarListAttribute; + namespace quantifiers { class SynthConjecture; diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 9906eef2f..904f301b9 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -43,35 +43,10 @@ typedef expr::Attribute TermDepthAttribute; struct ContainsUConstAttributeId {}; typedef expr::Attribute ContainsUConstAttribute; -//for bounded integers -struct BoundIntLitAttributeId {}; -typedef expr::Attribute BoundIntLitAttribute; - //for quantifier instantiation level struct QuantInstLevelAttributeId {}; typedef expr::Attribute QuantInstLevelAttribute; -//rewrite-rule priority -struct RrPriorityAttributeId {}; -typedef expr::Attribute RrPriorityAttribute; - -/** Attribute true for quantifiers that do not need to be partially instantiated */ -struct LtePartialInstAttributeId {}; -typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute; - -// attribute for associating a synthesis function with a first order variable -struct SygusSynthGrammarAttributeId {}; -typedef expr::Attribute - SygusSynthGrammarAttribute; - -// attribute for associating a variable list with a synth fun -struct SygusSynthFunVarListAttributeId {}; -typedef expr::Attribute SygusSynthFunVarListAttribute; - -//attribute for fun-def abstraction type -struct AbsTypeFunDefAttributeId {}; -typedef expr::Attribute AbsTypeFunDefAttribute; - /** Attribute for id number */ struct QuantIdNumAttributeId {}; typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; -- cgit v1.2.3