From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 16 Sep 2019 21:44:52 +0000 (-0500)
Subject: Move specific attributes out of term util (#3279)
X-Git-Tag: cvc5-1.0.0~3948
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9c4d548af9a14c18a6d69b41bba3e36054d37c0c;p=cvc5.git

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 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<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 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<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 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 <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 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<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 5832d2817..29aba0f1a 100644
--- 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 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 <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 9906eef2f..904f301b9 100644
--- 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;