mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
trail
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
549b984c88
commit
12ccd99e84
1 changed files with 30 additions and 0 deletions
30
src/math/polysat/trail.h
Normal file
30
src/math/polysat/trail.h
Normal file
|
@ -0,0 +1,30 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat trail
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "math/polysat/types.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
enum trail_instr_t {
|
||||
qhead_i,
|
||||
add_var_i,
|
||||
inc_level_i,
|
||||
viable_i,
|
||||
assign_i,
|
||||
just_i
|
||||
};
|
||||
|
||||
|
||||
|
||||
}
|
Loading…
Add table
Add a link
Reference in a new issue