diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/arrays/options | 8 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_instantiator.cpp | 3 |
3 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index e4c814660..8b8a5bd48 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -22,4 +22,5 @@ libarrays_la_SOURCES = \ theory_arrays_model.h \ theory_arrays_model.cpp -EXTRA_DIST = kinds +EXTRA_DIST = \ + kinds diff --git a/src/theory/arrays/options b/src/theory/arrays/options new file mode 100644 index 000000000..bf8afc589 --- /dev/null +++ b/src/theory/arrays/options @@ -0,0 +1,8 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module ARRAYS "theory/arrays/options.h" Arrays theory + +endmodule diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp index 67c42d124..f5a722737 100644 --- a/src/theory/arrays/theory_arrays_instantiator.cpp +++ b/src/theory/arrays/theory_arrays_instantiator.cpp @@ -17,6 +17,7 @@ #include "theory/theory_engine.h" #include "theory/arrays/theory_arrays_instantiator.h" #include "theory/arrays/theory_arrays.h" +#include "theory/quantifiers/options.h" #include "theory/rr_candidate_generator.h" using namespace std; @@ -38,7 +39,7 @@ void InstantiatorTheoryArrays::preRegisterTerm( Node t ){ void InstantiatorTheoryArrays::assertNode( Node assertion ){ Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl; d_quantEngine->addTermToDatabase( assertion ); - if( Options::current()->cbqi ){ + if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) ); }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ |