mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 00:20:50 +00:00
Code Activity

set up udoc relation to use datalog engine

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-01 17:19:50 -07:00
parent c4366e57f8
commit 94b981024e
2 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/model/model_core.h
View file

@ -72,8 +72,6 @@ public:
void unregister_decl(func_decl * d); void unregister_decl(func_decl * d);
func_interp* update_func_interp(func_decl* f, func_interp* fi); func_interp* update_func_interp(func_decl* f, func_interp* fi);
void add_lambda_defs();
virtual expr * get_some_value(sort * s) = 0; virtual expr * get_some_value(sort * s) = 0;
virtual expr * get_fresh_value(sort * s) = 0; virtual expr * get_fresh_value(sort * s) = 0;
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0; virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;

3
src/test/udoc_relation.cpp
View file

@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "muz/rel/udoc_relation.h" #include "muz/rel/udoc_relation.h"
#include "util/trace.h" #include "util/trace.h"
#include "util/gparams.h"
#include "util/vector.h" #include "util/vector.h"
#include "util/gparams.h" #include "util/gparams.h"
#include "ast/ast.h" #include "ast/ast.h"
@ -36,7 +37,7 @@ class udoc_tester {
struct init { struct init {
init(ast_manager& m) { init(ast_manager& m) {
gparams::set("fp.engine", "datalog"); gparams::set("fp.engine", "datalog");
reg_decl_plugins(m); reg_decl_plugins(m);
} }
}; };