Significant work on bounded integer quantification to handle non-trivial bounds. Refactoring of InstConstantAttribute to be internal to TermDb.

1 files changed, 4 insertions, 2 deletions

diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 92c866ffd..00a910567 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -65,8 +65,8 @@ public:
     d_has_simplified = false;

   }

   bool addEntry( FullModelChecker * m, Node c, Node v);

-  Node evaluate( FullModelChecker * m, std::vector<Node> inst );

-  int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst );

+  Node evaluate( FullModelChecker * m, std::vector<Node>& inst );

+  int getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst );

   void simplify( FullModelChecker * m );

   void debugPrint(const char * tr, Node op, FullModelChecker * m);

 };

@@ -141,6 +141,8 @@ public:
 

   /** process build model */

   void processBuildModel(TheoryModel* m, bool fullModel);

+  /** get current model value */

+  Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );

 };

 

 }