Move specific attributes out of term util (#3279)

diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index d668c6f02cc700bf30efe0b669e8045b1c319901..1333af61cb9bd54b0eebc77e6677316be2ddb00b 100644 (file)
--- 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<BoundIntLitAttributeId, uint64_t> 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 f3eb88a902bbc48e591f2cf36506e9e3b5084c19..caca25fde1a6291479c004a4764f40c9e1fa3731 100644 (file)
--- 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<bool>())
           {
             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 0282f0e407fcc61d103838836f45e3f6722cffcc..f98208abad021794290285e1b7b08bba913fb662 100644 (file)
--- 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 <iostream>
-#include <string>
-#include <vector>
 #include <map>
+#include <vector>
+#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<AbsTypeFunDefAttributeId, bool> 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 1cad52b4356a625fa817cd1b8d886d50c81f2d1d..d39ea3cfe569c2f4b6086bb18b7ebbcaad207e41 100644 (file)
--- 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<LtePartialInstAttributeId, bool>
+    LtePartialInstAttribute;
+
 namespace quantifiers {
 
 class LtePartialInst : public QuantifiersModule {

diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 5832d2817a82d22c7c89ac6f36028a717b32710b..29aba0f1aa8cc5fe0710b6d2a9ce672b8426c8e4 100644 (file)
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -21,12 +21,22 @@
 #include <map>
 #include <vector>
 
+#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<RrPriorityAttributeId, uint64_t> 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 7e72ecb4123cb55e10e7e201a47b842f8760901c..047a78d11b2f4ecf6c32d77d2d6f5e365a3fdd9d 100644 (file)
--- 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 b9f50f228ff67c2b5df85203a94466ee7b0f419f..ca1b9ae37ce10f3449aef111b81f503c42a485f7 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -21,6 +21,7 @@
 #include <map>
 #include <vector>
 
+#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<SygusSynthGrammarAttributeId, Node>
+    SygusSynthGrammarAttribute;
+
+/**
+ * Attribute for associating a function-to-synthesize with its formal argument
+ * list.
+ */
+struct SygusSynthFunVarListAttributeId
+{
+};
+typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node>
+    SygusSynthFunVarListAttribute;
+
 namespace quantifiers {
 
 class SynthConjecture;

diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 9906eef2fc864605af821dfac0902d08f7b13c87..904f301b91a91e5dbc646e4936ae6085ed01157f 100644 (file)
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -43,35 +43,10 @@ typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute;
 struct ContainsUConstAttributeId {};
 typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute;
 
-//for bounded integers
-struct BoundIntLitAttributeId {};
-typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
-
 //for quantifier instantiation level
 struct QuantInstLevelAttributeId {};
 typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttribute;
 
-//rewrite-rule priority
-struct RrPriorityAttributeId {};
-typedef expr::Attribute<RrPriorityAttributeId, uint64_t> 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<SygusSynthGrammarAttributeId, Node>
-    SygusSynthGrammarAttribute;
-
-// attribute for associating a variable list with a synth fun
-struct SygusSynthFunVarListAttributeId {};
-typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node> SygusSynthFunVarListAttribute;
-
-//attribute for fun-def abstraction type
-struct AbsTypeFunDefAttributeId {};
-typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
-
 /** Attribute for id number */
 struct QuantIdNumAttributeId {};
 typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;