options::arraysEagerIndexSplitting.set(false);
}
}
+ // Turn on array eager lemmas for QF_AX
+ if(! options::arraysEagerLemmas.wasSetByUser()) {
+ if (not d_logic.isQuantified() &&
+ d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+ d_logic.isPure(THEORY_ARRAY)) {
+ Trace("smt") << "setting array eager lemmas to true" << endl;
+ options::arraysEagerIndexSplitting.set(true);
+ }
+ }
// Turn on multiple-pass non-clausal simplification for QF_AUFBV
if(! options::repeatSimp.wasSetByUser()) {
bool repeatSimp = !d_logic.isQuantified() &&
option arraysEagerIndexSplitting --arrays-eager-index bool :default true :read-write
turn on eager index splitting for generated array lemmas
+option arraysEagerLemmas --arrays-eager-lemmas bool :default false :read-write
+ turn on eager lemma generation for arrays
+
endmodule
// Use static configuration of options for now
const bool d_ccStore = false;
const bool d_useArrTable = false;
-const bool d_eagerLemmas = false;
+ //const bool d_eagerLemmas = false;
const bool d_propagateLemmas = true;
const bool d_preprocess = true;
const bool d_solveWrite = true;
checkModel(e);
}
- if(!d_eagerLemmas && fullEffort(e) && !d_conflict && !options::arraysModelBased()) {
+ if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysModelBased()) {
// generate the lemmas on the worklist
Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
dischargeLemmas();
// TODO: maybe add triggers here
- if (d_eagerLemmas || bothExist) {
+ if (options::arraysEagerLemmas() || bothExist) {
// Make sure that any terms introduced by rewriting are appropriately stored in the equality database
Node aj2 = Rewriter::rewrite(aj);